Inference at * 2 2 2 1 
Iof proof for Lemma member nth tl:



1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. x : T
6. T List
7. u : T
8. v : T List
9. (x  nth_tl(n;v))  (x  v)
10. 0 < n
11. (x  nth_tl(n - 1;v))
  (x  [u / v]) 

latex

 by ((RWO "cons_member" 0) 
CollapseTHEN (Auto)) 

latex

C1: 

C1:   (x = u)  (x  v)
C.

Definitions	P  Q, P & Q, x:A  B(x), P  Q, t  T, P  Q, type List, x:A. B(x), x:AB(x), a < b, , Type, P  Q, left + right, s = t, (x  l)
Lemmas	cons member, l member wf